\begin{tabbing}
$\forall$${\it es}$:ES, $e$:E, $l$:IdLnk, ${\it tg}$:Id.
\\[0ex]($e$ sends on $l$ with tag ${\it tg}$)
\\[0ex]$\Rightarrow$ \=($\forall$${\it e'}$:E.\+
\\[0ex]($\uparrow$isrcv(${\it e'}$))
\\[0ex]$\Rightarrow$ (sender(${\it e'}$) = $e$)
\\[0ex]$\Rightarrow$ (lnk(${\it e'}$) = $l$)
\\[0ex]$\Rightarrow$ (tag(${\it e'}$) = ${\it tg}$)
\\[0ex]$\Rightarrow$ es{-}first{-}from(${\it es}$;$e$;$l$;${\it tg}$) $\leq$loc ${\it e'}$ )
\-
\end{tabbing}